1:=succ(0):nat.
2:=succ(1):nat.
3:=succ(2):nat.
4:=succ(3):nat.

lemma(x:nat):=eq_transitivity(nat,sum(x,1),succ(sum(x,0)),succ(x),sum_ax2(x,0),
  eq_functionality(nat,nat,sum(x,0),x,sum_ax1(x),succ)):is(sum(x,1),succ(x)).

2_plus_2:=eq_transitivity(nat,sum(2,2),succ(sum(2,1)),4,sum_ax2(2,1),
  eq_functionality(nat,nat,sum(2,1),3,lemma(2),succ)):is(sum(2,2),4).